TIMEOUT

We are left with following problem, upon which TcT provides the
certificate TIMEOUT.

Strict Trs:
  { #abs(#0()) -> #0()
  , #abs(#neg(@x)) -> #pos(@x)
  , #abs(#pos(@x)) -> #pos(@x)
  , #abs(#s(@x)) -> #pos(#s(@x))
  , *(@x, @y) -> #mult(@x, @y)
  , +(@x, @y) -> #add(@x, @y)
  , attach(@line, @m) -> attach#1(@line, @m)
  , attach#1(::(@x, @xs), @m) -> attach#2(@m, @x, @xs)
  , attach#1(nil(), @m) -> nil()
  , attach#2(::(@l, @ls), @x, @xs) ->
    ::(::(@x, @l), attach(@xs, @ls))
  , attach#2(nil(), @x, @xs) -> nil()
  , lineMult(@l, @m2) -> lineMult#1(@m2, @l)
  , lineMult#1(::(@x, @xs), @l) ->
    ::(mult(@l, @x), lineMult(@l, @xs))
  , lineMult#1(nil(), @l) -> nil()
  , mult(@l1, @l2) -> mult#1(@l1, @l2)
  , makeBase(@m) -> makeBase#1(@m)
  , makeBase#1(::(@l, @m')) -> mkBase(@l)
  , makeBase#1(nil()) -> nil()
  , mkBase(@m) -> mkBase#1(@m)
  , matrixMult(@m1, @m2) ->
    matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))
  , transAcc(@m, @base) -> transAcc#1(@m, @base)
  , matrixMult'(@m1, @m2) -> matrixMult'#1(@m1, @m2)
  , matrixMult'#1(::(@l, @ls), @m2) ->
    ::(lineMult(@l, @m2), matrixMult'(@ls, @m2))
  , matrixMult'#1(nil(), @m2) -> nil()
  , matrixMult3(@m1, @m2, @m3) ->
    matrixMult(matrixMult(@m1, @m2), @m3)
  , matrixMultList(@acc, @mm) -> matrixMultList#1(@mm, @acc)
  , matrixMultList#1(::(@m, @ms), @acc) ->
    matrixMultList(matrixMult(@acc, @m), @ms)
  , matrixMultList#1(nil(), @acc) -> @acc
  , matrixMultOld(@m1, @m2) -> matrixMult'(@m1, transpose(@m2))
  , transpose(@m) -> transpose#1(@m, @m)
  , mkBase#1(::(@l, @m')) -> ::(nil(), mkBase(@m'))
  , mkBase#1(nil()) -> nil()
  , mult#1(::(@x, @xs), @l2) -> mult#2(@l2, @x, @xs)
  , mult#1(nil(), @l2) -> #abs(#0())
  , mult#2(::(@y, @ys), @x, @xs) -> +(*(@x, @y), mult(@xs, @ys))
  , mult#2(nil(), @x, @xs) -> #abs(#0())
  , split(@m) -> split#1(@m)
  , split#1(::(@l, @ls)) -> split#2(@l, @ls)
  , split#1(nil()) -> tuple#2(nil(), nil())
  , split#2(::(@x, @xs), @ls) -> split#3(split(@ls), @x, @xs)
  , split#2(nil(), @ls) -> tuple#2(nil(), nil())
  , split#3(tuple#2(@ys, @m'), @x, @xs) ->
    tuple#2(::(@x, @ys), ::(@xs, @m'))
  , transAcc#1(::(@l, @m'), @base) ->
    attach(@l, transAcc(@m', @base))
  , transAcc#1(nil(), @base) -> @base
  , transpose#1(::(@xs, @xss), @m) -> transpose#2(split(@m))
  , transpose#1(nil(), @m) -> nil()
  , transpose#2(tuple#2(@l, @m')) -> transpose#3(@m', @l)
  , transpose#3(::(@y, @ys), @l) -> ::(@l, transpose(::(@y, @ys)))
  , transpose#3(nil(), @l) -> nil()
  , transpose'(@m) -> transAcc(@m, makeBase(@m)) }
Weak Trs:
  { #mult(#0(), #0()) -> #0()
  , #mult(#0(), #neg(@y)) -> #0()
  , #mult(#0(), #pos(@y)) -> #0()
  , #mult(#neg(@x), #0()) -> #0()
  , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
  , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
  , #mult(#pos(@x), #0()) -> #0()
  , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
  , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
  , #add(#0(), @y) -> @y
  , #add(#neg(#s(#0())), @y) -> #pred(@y)
  , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
  , #add(#pos(#s(#0())), @y) -> #succ(@y)
  , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
  , #pred(#0()) -> #neg(#s(#0()))
  , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
  , #pred(#pos(#s(#0()))) -> #0()
  , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
  , #succ(#0()) -> #pos(#s(#0()))
  , #succ(#neg(#s(#0()))) -> #0()
  , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
  , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
  , #natmult(#0(), @y) -> #0()
  , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y))
  , #natadd(#0(), @y) -> @y
  , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) }
Obligation:
  innermost runtime complexity
Answer:
  TIMEOUT

Computation stopped due to timeout after 300.0 seconds.

Arrrr..